es:ES, Fail:AbsInterface(Top), A:Type, X:AbsInterface(A), e:E.
((e  alive(X)))  (((e  X)) & ((e':E. ((e' <loc e) & ((e'  Fail)))))) 

latex

Definitions	alive(X), x:A  B(x), P & Q, P  Q, E, x:AB(x), x:A. B(x), AbsInterface(A), Type, Top, ES, A, b, (e <loc e'), x:A. B(x), P  Q, P  Q, x. t(x), e  X, (I|p), fail-dcdr{i:l}(es;Fail)
Lemmas	fail-dcdr wf, iff functionality wrt iff, es-is-interface-co-restrict, iff wf, rev implies wf, es-locl wf, not wf, assert wf, event system wf, top wf, es-interface wf, es-E wf